ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), es:event_system{i:l}, i:Id, e1,e2:{e:es-E(es)| 
ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), es:event_system{i:l}, i:Id, e1,e2:{loc(e) = i} .
(x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
 (e:es-E(es). 
 (loc(e) = i)  subtype_rel(es-valtype(es; e); fpf-cap(da; Kind-deq; es-kind(es; e); top)))
 (ks:(Knd List), T:Type, z:T, g:(k:{k:Knd| (k  ks)} decl-state(ds)fpf-cap(da;
 (ks:(Knd List), T:Type, z:T, g:(k:{k:Knd| (k  ks)} decl-state(ds)fpf-cap(Kind-deq;
 (ks:(Knd List), T:Type, z:T, g:(k:{k:Knd| (k  ks)} decl-state(ds)fpf-cap(k;
 (ks:(Knd List), T:Type, z:T, g:(k:{k:Knd| (k  ks)} decl-state(ds)fpf-cap(top)
 (ks:(Knd List), T:Type, z:T, g:(TT). es-trans-state-from{i:l}(es;ks;g;z;e1;e2)  T) 

latex

Definitions

t  T, Kind-deq, x:A. B(x), Knd, (x  l), b, prop{i:l}, A, b, , deq-member(eq; x; L), P  Q, P  Q, P  Q, Unit, spreadn(a; x,y,z.t(x;y;z)), x,y. t(x;y), list_accum(x,a.f(x;a); y; l), es-trans-state-from{i:l}(es;ks;g;z;e1;e2), top, x. t(x), fpf-cap(f; eq; x; z), decl-state(ds), EqDecider(T), fpf(A; a.B(a)), es-kind(es; e), es-valtype(es; e), loc(e), Id, es-E(es), id-deq, es-vartype(es; i; x), event_system{i:l}, es-hist{i:l}(es;e1;e2), event-info(ds;da)

Lemmas

fpf wf, event system wf, es-vartype wf, id-deq wf, es-E wf, Id wf, es-loc wf, es-valtype wf, es-kind wf, fpf-trivial-subtype-top, decl-state wf, fpf-cap wf, top wf, es-hist wf, list accum wf, event-info wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, deq-member wf, bool wf, bnot wf, not wf, assert wf, l member wf, Knd wf, Kind-deq wf